/FONT#0=BDR25/FONT#1=BDJ25/FONT#2=BDR25X/FONT#3=SUB/FONT#4=NGR30/FONT#5=NGR40
␈↓␈↓↓␈↓α␈↓β␈↓∧␈↓¬␈↓
␈↓ ↓H
(This version of this chapter is very incomplete and preliminary.)
␈↓ ↓H

␈↓ ↓H
␈↓¬␈↓ ¬jCHAPTER IV

␈↓ ↓H
␈↓ ¬.LISP SELF-APPLIED

␈↓ ↓H

␈↓ ↓H
␈↓∧1. The list representation of LISP functions.␈↓
␈↓ ↓H

␈↓ ↓H
␈↓ α_When␈α∪one␈α∪computes␈α∩with␈α∩symbolic␈α∩expressions,␈α∩it␈α∩is␈α∩necessary␈α∩to␈α∩face␈α∩the␈α∩fact␈α∩that␈α∩the␈α∩most
␈↓ ↓Hconvenient␈αnotation␈αfor␈αreading␈αand␈αwriting␈αis␈αnot␈αthe␈αmost␈αconvenient␈αnotation␈αfor␈αsymbolic␈αdata␈αfrom␈αthe
␈↓ ↓Hpoint␈α∂of␈α∂view␈α∂of␈α∂the␈α∂programmer␈α∂who␈α∂must␈α∂write␈α∂programs␈α∞for␈α∞manipulating␈α∞the␈α∞data.␈α∞So␈α∞far,␈α∞we␈α∞have
␈↓ ↓Hresolved␈α⊃this␈α⊃dilemma␈α⊃by␈α⊃using␈α⊃S-expressions␈α⊃for␈α⊃data␈α⊃and␈α⊃writing␈α⊃LISP␈α⊂functions␈α⊂and␈α⊂programs␈α⊂in␈α⊂a
␈↓ ↓Hlanguage␈α⊃that␈α⊃is␈α⊃hopefully␈α⊃convenient␈α⊃for␈α⊃reading␈α⊃and␈α⊃writing.␈α⊃Now␈α⊃LISP␈α⊃programs␈α⊃are␈α⊂also␈α⊂symbolic
␈↓ ↓Hinformation,␈α∞and␈α∞we␈α∞want␈α
to␈α
be␈α
able␈α
to␈α
manipulate␈α
LISP␈α
programs␈α
with␈α
LISP␈α
functions␈α
and␈α
programs.␈α
In
␈↓ ↓Horder␈α∞to␈α∞do␈α∞this␈α∞we␈α∞use␈α∞a␈α∞representation␈α∞of␈α∞LISP␈α∞functions␈α
by␈α
LISP␈α
lists.␈α
In␈α
Chapter␈α
6,␈α
we␈α
shall␈α
discuss
␈↓ ↓Hprocedures␈α
for␈α
translating␈α
between␈α
S-expression␈α
notation␈α
and␈α
other␈α
notations␈α
for␈α
symbolic␈α
information.

␈↓ α_We␈α
use␈α
the␈α
following␈α
conventions:

␈↓ α_1.␈α
Variables␈α
are␈α
represented␈α
by␈αatomic␈αsymbols␈αcomposed␈αof␈αupper␈αcase␈αletters.␈αThus␈αthe␈αvariable␈α␈↓↓x␈↓
␈↓ ↓Hwill␈α
normally␈α
be␈α
represented␈α
by␈α
the␈α
corresponding␈α
upper␈α
case␈α
letter␈α
X.

␈↓ α_2.␈αAn␈αS-expression␈α␈↓↓e␈↓␈αwill␈αbe␈αrepresented␈αas␈α(QUOTE␈α␈↓↓e␈↓).␈αThus␈αthe␈αatom␈αX␈αis␈αrepresented␈αby␈α(QUOTE
␈↓ ↓HX).

␈↓ α_3.␈α∞The␈α∞basic␈α∞LISP␈α∞functions␈α∞␈↓↓car,␈α∞cdr,␈α
cons,␈α
atom␈↓␈α
and␈α
␈↓↓eq␈↓,␈α
the␈α
functions␈α
␈↓↓list␈↓␈α
and␈α
␈↓↓null␈↓␈α
derived␈α
from
␈↓ ↓Hthem␈α∞are␈α∞represented␈α∞by␈α∞writing␈α∞the␈α∞words␈α∞in␈α∞upper␈α∞case.␈α∞Thus␈α∞we␈α∞have␈α∞CAR,␈α∞CDR,␈α
CONS,␈α
ATOM,␈α
EQ,
␈↓ ↓HLIST,␈α
and␈α
NULL.␈α
Defined␈α
functions␈α
are␈α
also␈α
represented␈α
by␈α
atoms,␈α
e.g.␈α
ALT,␈α
DIFF,␈α
etc.

␈↓ α_4.␈α⊃Numbers␈α⊃are␈α⊃represented␈α⊂by␈α⊂the␈α⊂S-expression␈α⊂notation␈α⊂for␈α⊂numbers␈α⊂without␈α⊂QUOTE,␈α⊂and␈α⊂the
␈↓ ↓Hspecial␈α⊂atoms␈α⊂T␈α⊂and␈α⊂NIL␈α⊂are␈α⊂represented␈α⊂by␈α∂themselves␈α∂without␈α∂QUOTE.␈α∂Avoiding␈α∂QUOTE␈α∂here␈α∂is␈α∂for
␈↓ ↓Hconvenience␈α⊗and␈α⊗can␈α⊗be␈α∃regarded␈α∃as␈α∃using␈α∃variables␈α∃T␈α∃and␈α∃NIL␈α∃whose␈α∃permanent␈α∃values␈α∃are␈α∃the
␈↓ ↓HS-expressions␈α
T␈α
and␈α
NIL.

␈↓ α_5.␈α
The␈α
application␈α
of␈α
a␈α
function␈α
to␈α
arguments␈α
is␈αrepresented␈αby␈αa␈αlist␈αthe␈αfirst␈αelement␈αof␈αwhich␈αis
␈↓ ↓Hthe␈α∩function␈α∩name␈α∩and␈α∩the␈α∩remaining␈α∩elements␈α∩are␈α∩the␈α⊃arguments␈α⊃in␈α⊃the␈α⊃same␈α⊃order.␈α⊃Thus␈α⊃␈↓↓f[x,y]␈↓␈α⊃is
␈↓ ↓Hrepresented␈α
by␈α
(F␈α
X␈α
Y).

␈↓ ↓H
␈↓ α_6. The conditional expression
␈↓ ↓H

␈↓ ↓H
␈↓ α_␈↓αif␈↓↓ p␈↓β1␈↓α then ␈↓↓e␈↓β1␈↓↓ ... ␈↓αelse if ␈↓↓p␈↓βn␈↓α then ␈↓↓e␈↓βn␈↓
␈↓ ↓H

␈↓ ↓H
is represented by
␈↓ ↓H

␈↓ ↓H
␈↓ α_(COND (␈↓↓p␈↓β1␈↓↓ e␈↓β1␈↓↓) ... (␈↓↓p␈↓βn␈↓↓ e␈↓βn␈↓)).
␈↓ ↓H

␈↓ ↓H
There is no way of representing a final ␈↓αelse␈↓, so
␈↓ ↓H

␈↓ ↓H
␈↓ α_␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse ␈↓↓b␈↓
␈↓ ↓H

␈↓ ↓H
is represented by
␈↓ ↓H

␈↓ ↓H
␈↓ α_(COND (␈↓↓p a)(␈↓T ␈↓↓b␈↓)).
␈↓ ↓H

␈↓ ↓H
Thus
␈↓ ↓H

␈↓ ↓H
␈↓ α_␈↓αif n ␈↓↓u ∨ ␈↓αn d ␈↓↓u ␈↓αthen␈↓↓ u ␈↓αelse a ␈↓↓u . ␈↓↓alt ␈↓αdd ␈↓↓u␈↓
␈↓ ↓H

␈↓ ↓H
is represented by
␈↓ ↓H

␈↓ ↓H
␈↓ α_(COND ((OR (NULL U) (NULL (CDR U))) U) (T (CONS (CAR U) (ALT (CDDR U))))).
␈↓ ↓H

␈↓ ↓H
␈↓ α_7.␈α
The␈α
λ-expression␈α
λ␈↓↓x...z.e␈↓␈α
is␈α
represented␈α
by␈α
(LAMBDA␈α
(X␈α
...␈α
Z)␈α
␈↓↓e␈↓).␈α
Thus

␈↓ ↓H
␈↓ α_λ␈↓↓x y.␈↓αif n ␈↓↓x ␈↓α then ␈↓↓y ␈↓αelse a ␈↓↓x . append[␈↓αd ␈↓↓x,y]␈↓
␈↓ ↓H

␈↓ ↓H
is represented by
␈↓ ↓H

␈↓ ↓H
␈↓ α_(LAMBDA (X Y) (COND ((NULL X) Y) (T (CONS (CAR X) (APPEND (CDR X) Y)))))).
␈↓ ↓H

␈↓ ↓H
␈↓ α_8.␈α
Finally,␈α
␈↓αlabel␈↓↓[fname,e]␈↓␈α
is␈α
represented␈α
by␈α
(LABEL␈α
␈↓↓fname␈α
e),␈α
so␈α
that

␈↓ ↓H
␈↓ α_␈↓αlabel␈↓↓[alt,␈↓λ␈↓↓x.␈↓αif n ␈↓↓x ∨ ␈↓αn d ␈↓↓x ␈↓αthen ␈↓↓x ␈↓αelse a ␈↓↓x . alt[␈↓αdd␈↓↓ x]]␈↓
␈↓ ↓H

␈↓ ↓H
is represented by
␈↓ ↓H

␈↓ ↓H
␈↓ α_(LABEL ALT (LAMBDA (X) (COND ((OR (NULL X) (NULL (CDR X))) X)
␈↓ ↓H
␈↓ α_␈↓ αh(T (CONS (CAR X) (ALT (CDDR X))))))).
␈↓ ↓H

␈↓ ↓H
␈↓ α_Actually,␈α
␈↓αlabel␈↓␈α
is␈α
rarely␈α
used␈α
in␈α
LISP␈α
programming,␈α
because␈α
it␈α
names␈αa␈αfunction␈αfor␈αimmediate␈αuse
␈↓ ↓Honly,␈αand␈αusually␈αone␈αwants␈αto␈αattach␈αa␈αfunction␈αdefinition␈αto␈αits␈αname␈αfor␈αlater␈αuse␈αin␈αseveral␈αplaces␈α
in␈α
the
␈↓ ↓Hprogram.␈α
The␈α
notation␈α
for␈α
making␈α
definitions␈α
varies␈α
with␈α
the␈α
implementation␈α
of␈α
LISP.

␈↓ ↓H␈↓∧2.␈α
The␈α
function␈α
␈↓↓eval␈↓.

␈↓ α_Except␈α
for␈α
speed␈α
and␈αmemory␈αsize␈αall␈αpresent␈αday␈αstored␈αprogram␈αcomputers␈αare␈αequivalent␈αin␈αwhat
␈↓ ↓Hcomputations␈αthey␈αcan␈αdo.␈αA␈αprogram␈αwritten␈αfor␈αone␈αcomputer␈αcan␈α
be␈α
translated␈α
to␈α
run␈α
on␈α
another.␈α
Indeed,
␈↓ ↓Hone␈αcan␈αwrite␈αa␈αsimulator␈αfor␈αone␈αcomputer␈αto␈αrun␈αon␈αanother.␈αTo␈αput␈αit␈αin␈αcommercial␈αterms,␈αno␈αcomputer
␈↓ ↓Hmanufacturer␈α∂can␈α∂advertise␈α∂that␈α∞his␈α∞machine␈α∞can␈α∞do␈α∞calculations␈α∞impossible␈α∞on␈α∞the␈α∞machine␈α∞made␈α∞by␈α∞his
␈↓ ↓Hcompetitors.

␈↓ α_This␈α
is␈α
well␈α
known␈αintuitively,␈αand␈αthe␈αfirst␈αmathematical␈αtheorem␈αof␈αthis␈αkind␈αwas␈αproved␈αby␈αA.M.
␈↓ ↓HTuring␈α
(1936),␈α
who␈αdefined␈αa␈αprimitive␈αkind␈αof␈αcomputer␈αnow␈αcalled␈αa␈αTuring␈αmachine,␈αand␈αshowed␈αhow␈αto
␈↓ ↓Hmake␈α⊃a␈α⊃universal␈α⊃machine␈α⊃that␈α⊃could␈α⊃do␈α⊃any␈α⊃computation␈α⊃done␈α⊃by␈α⊃any␈α⊃Turing␈α⊂machine␈α⊂when␈α⊂given␈α⊂a
␈↓ ↓Hdescription␈α
of␈α
the␈α
machine␈α
to␈α
be␈α
simulated␈α
and␈α
the␈α
initial␈α
tape␈α
of␈α
the␈α
computation␈α
to␈α
be␈α
imitated.

␈↓ α_In␈αLISP␈α
the␈α
function␈α
␈↓↓eval␈↓␈α
is␈α
a␈α
universal␈α
LISP␈α
function␈α
in␈α
the␈α
sense␈α
that␈α
any␈α
computation␈α
done␈α
by␈α
any
␈↓ ↓HLISP␈α
function␈α
can␈α
be␈α
done␈α
by␈α
␈↓↓eval␈↓␈α
when␈α
␈↓↓eval␈↓␈α
is␈α
given␈α
suitable␈α
arguments.

␈↓ α_␈↓↓eval␈↓␈αhas␈αtwo␈αarguments␈αthe␈αfirst␈αof␈αwhich␈αis␈αa␈αLISP␈αexpression␈αin␈αthe␈αnotation␈αgiven␈αin␈α
the␈α
previous
␈↓ ↓Hsection,␈αwhile␈αthe␈αsecond␈αis␈αa␈αlist␈αof␈αpairs␈αthat␈αgive␈αthe␈αvalues␈αof␈αany␈αfree␈αvariables␈αthat␈αmay␈αoccur␈αin␈αthe
␈↓ ↓Hexpression.␈α
Since␈α
any␈α
computation␈α
can␈α
be␈α
described␈αas␈αevaluating␈αan␈αexpression␈αwithout␈αfree␈αvariables,␈αthe
␈↓ ↓Hsecond␈αargument␈αplays␈αa␈αrole␈αmainly␈αin␈αthe␈αrecursive␈αdefinition␈αof␈α␈↓↓eval␈↓,␈αand␈αwe␈αcan␈αstart␈αour␈αcomputations
␈↓ ↓Hwith␈α
the␈α
second␈α
argument␈α
NIL.

␈↓ α_To␈αillustrate␈αthis,␈αsuppose␈αwe␈αwant␈αto␈αapply␈αthe␈αfunction␈α␈↓↓alt␈↓␈αto␈αthe␈αlist␈α(A␈αB␈αC␈αD␈αE),␈αi.e.␈αwe␈αwish␈αto
␈↓ ↓Hevaluate␈α
␈↓↓alt␈↓[(A␈α
B␈α
C␈α
D␈α
E)].␈α
This␈α
can␈α
be␈α
obtained␈α
by␈α
computing

␈↓ α_␈↓↓eval␈↓[((LABEL␈α
ALT␈α
(LAMBDA␈α
(X)␈α
(COND␈α
((OR␈α
(NULL␈α
X)␈α
(NULL␈α(CDR␈αX)))␈αX)␈α(T␈α(CONS␈α(CAR␈αX)
␈↓ ↓H(ALT␈α
(CDDR␈α
X)))))))␈α
(QUOTE␈α
(A␈α
B␈α
C␈α
D␈α
E)),NIL],

␈↓ ↓Hand␈αgives␈αthe␈αexpected␈αresult␈α(A␈α
C␈α
E).␈α
The␈α
second␈α
argument␈α
of␈α
␈↓↓eval␈↓,␈α
taken␈α
as␈α
NIL␈α
in␈α
the␈α
above␈α
example␈α
is␈α
a
␈↓ ↓Hlist␈αof␈αdotted␈αpairs␈αwhere␈αthe␈αfirst␈αelement␈αof␈αeach␈αpair␈αis␈αan␈αatom␈αrepresenting␈αa␈αvariable␈αand␈αthe␈αsecond
␈↓ ↓Helement␈α∞is␈α∞the␈α∞value␈α∞assigned␈α∞to␈α∞that␈α∞variable.␈α∞A␈α∞variable␈α∞may␈α∞occur␈α∞more␈α∞than␈α∞once␈α
in␈α
the␈α
list␈α
and␈α
the
␈↓ ↓Hvalue␈α
chosen␈α
is␈α
that␈α
paired␈α
with␈α
the␈α
first␈α
occurrence␈α
of␈α
the␈α
variable.␈α
We␈α
illustrate␈α
this␈α
by␈α
the␈α
equation

␈↓ α_␈↓↓eval␈↓[(CAR␈α
X),((X.(B.C))␈α
(Y.A)␈α
(X.B))]␈α
=␈α
B,

␈↓ ↓Hi.e.␈α
we␈α
have␈α
evaluated␈α
␈↓αa␈α
␈↓↓x␈↓␈α
with␈α
␈↓↓␈α
x␈↓␈α
=␈α
(B.C).␈α
The␈α
value␈α
associated␈α
with␈αa␈αvariable␈αin␈αsuch␈αa␈αlist␈αof␈αpairs␈αis
␈↓ ↓Hcomputed␈α
by␈α
the␈α
auxiliary␈α
function␈α
␈↓↓assoc␈↓␈α
which␈α
has␈α
the␈α
recursive␈α
definition

␈↓ ↓H
␈↓ α_␈↓↓assoc[v,a] ← ␈↓αif n ␈↓↓a ␈↓αthen ␈↓NIL ␈↓αelse if aa ␈↓↓a␈↓α eq ␈↓↓v ␈↓αthen a ␈↓↓a ␈↓αelse ␈↓↓alt[v,␈↓αd ␈↓↓a]␈↓.
␈↓ ↓H

␈↓ ↓H
Thus we have ␈↓↓assoc␈↓[X,((X.(B.C)) (Y.A) (X.B))] = (X.(B.C)).
␈↓ ↓H

␈↓ ↓H
␈↓ α_A simplified version of the usual LISP ␈↓↓eval␈↓ is the following:
␈↓ ↓H

␈↓ ↓H
␈↓↓eval[e,a] ←
␈↓ ↓H
␈↓ α_␈↓αif at ␈↓↓e ␈↓αthen ␈↓[␈↓αif numberp ␈↓↓e ∨ e ␈↓αeq ␈↓NIL ∨ ␈↓↓e ␈↓αeq ␈↓T ␈↓αthen ␈↓↓e ␈↓αelse␈↓↓ assoc[e,a]]
␈↓ ↓H
␈↓ α_␈↓αelse if at a␈↓↓ e ␈↓αthen
␈↓ ↓H
␈↓ α_␈↓ αh␈↓↓[␈↓αif a ␈↓↓e␈↓α eq ␈↓CAR ␈↓αthen a ␈↓↓eval[␈↓αad ␈↓↓e,a]
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse if a ␈↓↓e␈↓α eq ␈↓CDR ␈↓αthen d ␈↓↓eval[␈↓αad ␈↓↓e,a]
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse if a ␈↓↓e␈↓α eq ␈↓CONS ␈↓αthen ␈↓↓eval[␈↓αad ␈↓↓e,a] . eval[␈↓αadd ␈↓↓e,a]
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse if a ␈↓↓e␈↓α eq ␈↓ATOM ␈↓αthen at ␈↓↓eval[␈↓αad ␈↓↓e,a]
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse if a ␈↓↓e␈↓α eq ␈↓EQ ␈↓αthen at ␈↓↓eval[␈↓αad ␈↓↓e,a] ␈↓αeq ␈↓↓eval[␈↓αadd ␈↓↓e,a]
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse if a ␈↓↓e␈↓α eq ␈↓QUOTE ␈↓αthen ad ␈↓↓e
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse if a ␈↓↓e␈↓α eq ␈↓COND ␈↓αthen ␈↓↓evcon[␈↓αd ␈↓↓e,a]
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse if a ␈↓↓e␈↓α eq ␈↓LIST ␈↓αthen ␈↓↓mapcar[␈↓αd ␈↓↓e,λx.eval[x,a]]
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse ␈↓↓eval[␈↓αd ␈↓↓assoc[␈↓αa ␈↓↓e,a] . ␈↓αd ␈↓↓e,a]]
␈↓ ↓H
␈↓ α_␈↓αelse if aa ␈↓↓e ␈↓αeq ␈↓LAMBDA ␈↓αthen ␈↓↓eval[␈↓αadda ␈↓↓e,prup[␈↓αada ␈↓↓e,mapcar[␈↓αd ␈↓↓e,λx.eval[x,a]]] . a]
␈↓ ↓H
␈↓ α_␈↓αelse if aa ␈↓↓e ␈↓αeq ␈↓LABEL ␈↓αthen␈↓↓eval[␈↓αadda ␈↓↓e . ␈↓αd ␈↓↓e,[␈↓αada ␈↓↓e . ␈↓αa ␈↓↓e] . a]␈↓,
␈↓ ↓H

␈↓ ↓H
where the auxiliary function ␈↓↓evcon␈↓ is defined by
␈↓ ↓H

␈↓ ↓H
␈↓ α_␈↓↓evcon[u,a] ← ␈↓αif ␈↓↓eval[␈↓αaa ␈↓↓u,a] ␈↓αthen ␈↓↓eval[␈↓αada ␈↓↓u,a] ␈↓αelse ␈↓↓evcon[␈↓αd ␈↓↓u,a]␈↓,
␈↓ ↓H

␈↓ ↓H
␈↓ ↓Hand␈α
the␈α
auxiliary␈α
function␈α
␈↓↓prup␈↓␈α
used␈α
for␈α
pairing␈α
up␈α
the␈α
elements␈α
of␈α
two␈α
lists␈α
of␈α
equal␈α
length␈α
is␈α
defined␈α
by

␈↓ ↓H
␈↓ α_␈↓↓prup[u,v] ← ␈↓αif n ␈↓↓u ␈↓αthen ␈↓NIL ␈↓αelse ␈↓↓[␈↓αa ␈↓↓u . ␈↓αa ␈↓↓v] . prup[␈↓αd ␈↓↓u,␈↓αd ␈↓↓u].␈↓
␈↓ ↓H

␈↓ ↓H
␈↓ α_The␈αway␈α␈↓↓eval␈↓␈αworks␈αshould␈αbe␈αclear;␈αatoms␈αare␈αeither␈αimmediately␈αevaluable␈αor␈αhave␈αto␈α
be␈α
looked␈α
up
␈↓ ↓Hon␈αthe␈αlist␈α␈↓↓a␈↓;␈αexpressions␈αwhose␈αfirst␈αterm␈αis␈αone␈αof␈αthe␈αelementary␈αfunctions␈αare␈αevaluated␈αby␈αperforming
␈↓ ↓Hthe␈αindicated␈αoperation␈αon␈αthe␈αresult␈αof␈αevaluating␈αthe␈αarguments;␈α␈↓↓list␈↓␈αhas␈αto␈αbe␈αhandled␈αspecially,␈αbecause
␈↓ ↓Hit␈αhas␈αan␈αindefinite␈αnumber␈αof␈αarguments;␈αconditionals␈αare␈αhandled␈αby␈αan␈αauxiliary␈αfunction␈αthat␈αevaluates
␈↓ ↓Hthe␈α∀terms␈α∀in␈α∀the␈α∀right␈α∀order;␈α∪quoted␈α∪S-expressions␈α∪are␈α∪trivial;␈α∪non-elementary␈α∪functions␈α∪have␈α∪their
␈↓ ↓Hdefinitions␈α
looked␈α
up␈α
on␈α
␈↓↓a␈↓␈α
and␈α
substituted␈α
for␈α
their␈αnames;␈αwhen␈αa␈αfunction␈αis␈αspecified␈αby␈αa␈αλ,␈αthe␈αinner
␈↓ ↓Hexpression␈α
is␈α
evaluated␈α
with␈α
a␈α
new␈α
␈↓↓a␈↓␈α
which␈α
is␈α
obtained␈αby␈αevaluating␈αthe␈αarguments␈αand␈αpairing␈αthem␈αup
␈↓ ↓Hwith␈αthe␈αvariables␈αand␈αputting␈αthem␈αon␈αthe␈αfront␈αof␈αthe␈αold␈α␈↓↓a␈↓;␈αand␈αfinally,␈α␈↓αlabel␈↓␈αis␈αhandled␈αby␈αpairing␈αthe
␈↓ ↓Hname␈α
of␈α
the␈α
function␈α
with␈α
the␈α
expression␈α
on␈α
␈↓↓a␈↓␈α
and␈α
replacing␈α
the␈α
whole␈α
function␈α
by␈α
the␈α
λ-part.

␈↓ α_␈↓↓eval␈↓␈α∂plays␈α∞both␈α∞a␈α∞theoretical␈α∞and␈α∞a␈α∞practical␈α∞role␈α∞in␈α∞LISP.␈α∞Historically,␈α∞the␈α∞list␈α∞notation␈α∞for␈α∞LISP
␈↓ ↓Hfunctions␈αand␈α␈↓↓eval␈↓␈αwere␈αfirst␈αdevised␈αin␈αorder␈αto␈αshow␈αhow␈αeasy␈αit␈αis␈αto␈αdefine␈αa␈αuniversal␈α
function␈α
in␈α
LISP
␈↓ ↓H-␈α
the␈α
idea␈α
was␈α
to␈α
advocate␈α
LISP␈α
as␈α
an␈αalternative␈αto␈αTuring␈αmachines␈αfor␈αdoing␈αthe␈αelementary␈αtheory␈αof
␈↓ ↓Hcomputability.␈α⊂The␈α⊂notation␈α⊂used␈α⊂was␈α⊂chosen␈α⊂without␈α⊂much␈α∂regard␈α∂for␈α∂human␈α∂convenience,␈α∂because␈α∂the
␈↓ ↓Horiginal␈α⊗idea␈α⊗was␈α⊗purely␈α⊗theoretical;␈α⊗the␈α⊗notation␈α⊗for␈α∃conditional␈α∃expressions,␈α∃for␈α∃example,␈α∃has␈α∃an
␈↓ ↓Hunnecessary␈αextra␈αlevel␈αof␈αparentheses.␈αHowever,␈αS.␈αR.␈αRussell␈αnoted␈αthat␈α␈↓↓eval␈↓␈αcould␈αserve␈αas␈αan␈αinterpreter
␈↓ ↓Hfor␈αLISP␈αand␈αpromptly␈αprogrammed␈αit␈αin␈αmachine␈αlanguage␈αwith␈αminor␈αmodifications␈αfor␈αpractical␈α
purposes.
␈↓ ↓HSince␈αa␈αcompiler␈αwas␈αlong␈αdelayed,␈αthe␈αinterpreter␈αwas␈αmore␈α
easily␈α
modified␈α
and␈α
handled␈α
some␈α
difficult␈α
cases
␈↓ ↓Hwith␈α⊃functional␈α⊃arguments␈α⊃better,␈α⊃an␈α⊃interpreter␈α⊃based␈α⊃on␈α⊃␈↓↓eval␈↓␈α⊃has␈α⊂remained␈α⊂a␈α⊂feature␈α⊂of␈α⊂most␈α⊂LISP
␈↓ ↓Hsystems.

␈↓ α_The␈α∞way␈α∞␈↓↓eval␈↓␈α∞handles␈α∞arguments␈α∞corresponds␈α∞to␈α∞the␈α∞call-by-value␈α
method␈α
of␈α
parameter␈α
passing␈α
in
␈↓ ↓HALGOL␈α
and␈α
similar␈α
languages.␈α
There␈α
is␈α
also␈α
a␈α
form␈α
of␈α
␈↓↓eval␈↓␈α
that␈α
corresponds␈α
to␈α
call-by-name.␈α
Here␈α
it␈α
is:

␈↓ ↓H
␈↓ α_␈↓↓neval[e,a] ← ␈↓αif at ␈↓↓e␈↓α then
␈↓ ↓H
␈↓ α_␈↓ αh␈↓↓[␈↓αif ␈↓↓e ␈↓αeq ␈↓T ␈↓α then ␈↓T
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse if ␈↓↓e ␈↓αeq ␈↓NIL ␈↓αthen ␈↓NIL
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse if ␈↓↓numberp e ␈↓αthen ␈↓↓e
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse ␈↓↓neval[␈↓αd ␈↓↓assoc[e,a],a]]
␈↓ ↓H

␈↓ ↓H
␈↓ α_␈↓αelse if at a ␈↓↓e ␈↓α then
␈↓ ↓H
␈↓ α_␈↓ αh␈↓↓[␈↓αif a ␈↓↓e ␈↓αeq ␈↓CAR ␈↓αthen a ␈↓↓neval[␈↓αad ␈↓↓e,a]
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse if a ␈↓↓e ␈↓αeq ␈↓CDR ␈↓αthen d ␈↓↓neval[␈↓αad ␈↓↓e,a]
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse if a ␈↓↓e ␈↓αeq ␈↓CONS ␈↓αthen ␈↓↓neval[␈↓αad ␈↓↓e,a] . neval[␈↓αadd ␈↓↓e,a]
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse if a ␈↓↓e ␈↓αeq ␈↓ATOM ␈↓αthen at ␈↓↓neval[␈↓αad ␈↓↓e,a]
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse if a ␈↓↓e ␈↓αeq ␈↓EQ ␈↓αthen ␈↓↓neval[␈↓αad ␈↓↓e,a] ␈↓αeq ␈↓↓neval[␈↓αadd ␈↓↓e,a]
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse if a ␈↓↓e ␈↓αeq ␈↓QUOTE ␈↓αthen ad ␈↓↓e
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse if a ␈↓↓e ␈↓αeq ␈↓COND ␈↓αthen ␈↓↓nevcon[␈↓αd ␈↓↓e,a]
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse if a ␈↓↓e ␈↓αeq ␈↓LIST ␈↓αthen ␈↓↓mapcar[␈↓αd ␈↓↓e,λx.neval[x,a]]
␈↓ ↓H
␈↓ α_␈↓ αh␈↓αelse ␈↓↓neval[␈↓αd ␈↓↓assoc[␈↓αa ␈↓↓e,a] . ␈↓αd ␈↓↓e,a]]
␈↓ ↓H

␈↓ ↓H
␈↓ α_␈↓αelse if aa ␈↓↓e ␈↓αeq ␈↓LAMBDA ␈↓αthen ␈↓↓neval[␈↓αadda ␈↓↓e,prup[␈↓αada ␈↓↓e,␈↓αd ␈↓↓e] . a]
␈↓ ↓H

␈↓ ↓H
␈↓ α_␈↓αelse if aa ␈↓↓e ␈↓αeq ␈↓LABEL ␈↓αthen ␈↓↓neval[␈↓αadda ␈↓↓e . ␈↓αd ␈↓↓e, [␈↓αada ␈↓↓e . ␈↓αa ␈↓↓e] . a],␈↓
␈↓ ↓H

␈↓ ↓H
where the auxiliary function ␈↓↓nevcon␈↓ is given by
␈↓ ↓H

␈↓ ↓H
␈↓ α_␈↓↓nevcon[u,a] ← ␈↓αif ␈↓↓neval[␈↓αaa ␈↓↓u,a] ␈↓αthen ␈↓↓neval[␈↓αada ␈↓↓u,a] ␈↓αelse ␈↓↓nevcon[␈↓αd ␈↓↓u,a].␈↓
␈↓ ↓H

␈↓ ↓H
␈↓ α_The␈αdifference␈αbetween␈α␈↓↓eval␈↓␈αand␈α␈↓↓neval␈↓␈αis␈αonly␈αin␈αtwo␈αterms.␈α␈↓↓eval␈↓␈αevaluates␈αa␈αvariable␈αby␈αlooking␈αit
␈↓ ↓Hup␈α⊃on␈α⊃the␈α⊃association␈α⊃list␈α⊃whereas␈α⊃␈↓↓neval␈↓␈α⊃looks␈α⊃it␈α⊃up␈α⊃on␈α⊃the␈α⊃association␈α⊃list␈α⊂and␈α⊂evaluates␈α⊂the␈α⊂result.
␈↓ ↓HCorrespondingly,␈αwhen␈αa␈αλ-expression␈αis␈αencountered,␈α
␈↓↓eval␈↓␈α
forms␈α
a␈α
new␈α
association␈α
list␈α
by␈α
pairing␈α
the␈α
values
␈↓ ↓Hof␈α⊃the␈α⊃arguments␈α⊃with␈α⊃the␈α⊃variables␈α⊃bound␈α⊃by␈α⊃the␈α⊃λ␈α⊃and␈α⊃putting␈α⊃the␈α⊃new␈α⊃pairs␈α⊃in␈α⊃front␈α⊃of␈α⊂the␈α⊂old
␈↓ ↓Hassociation␈α∂list,␈α∂whereas␈α∂␈↓↓neval␈↓␈α∂pairs␈α∂the␈α∂arguments␈α∞themselves␈α∞with␈α∞the␈α∞variables␈α∞and␈α∞puts␈α∞them␈α∞on␈α∞the
␈↓ ↓Hfront␈αof␈αthe␈αassociation␈αlist.␈αIn␈αmost␈αcases␈αboth␈αgive␈αthe␈αsame␈αresult␈αwith␈α
the␈α
same␈α
work,␈α
but␈α
␈↓↓neval␈↓␈α
gives␈α
a
␈↓ ↓Hresult␈α
in␈α
some␈α
cases␈α
in␈α
which␈α
␈↓↓eval␈↓␈α
loops.␈α
An␈α
example␈α
is␈α
obtained␈α
by␈α
evaluating␈α
␈↓↓F[2,1]␈↓␈α
where␈α
␈↓↓F␈↓␈α
is␈α
defined␈α
by

␈↓ ↓H
␈↓ α_␈↓↓F[x,y] ← ␈↓αif␈↓↓ x=0 ␈↓αthen ␈↓↓0 ␈↓αelse ␈↓↓F[x-1,F[y-2,x]].␈↓
␈↓ ↓H

␈↓ ↓H
Exercises
␈↓ ↓H

␈↓ ↓H
␈↓ α_1.␈α
Write␈α
␈↓↓neval␈↓␈α
and␈α
the␈α
necessary␈α
auxiliary␈α
functions␈α
in␈α
list␈α
form,␈α
and␈α
try␈α
them␈α
out␈α
on␈α
some␈α
examples.

␈↓ ↓H␈↓∧3.␈α
Computability.␈↓

␈↓ α_Some␈α∞LISP␈α∞calculations␈α∞run␈α∞on␈α∞indefinitely.␈α∞The␈α∞most␈α∞trivial␈α∞case␈α∞occurs␈α∞if␈α
we␈α
make␈α
the␈α
recursive
␈↓ ↓Hdefinition

␈↓ ↓H
␈↓ α_␈↓↓loop x ← loop x␈↓
␈↓ ↓H

␈↓ ↓H
␈↓ ↓Hand␈α⊂attempt␈α⊂to␈α∂compute␈α∂␈↓↓loop[x]␈↓␈α∂for␈α∂any␈α∂␈↓↓x␈↓␈α∂whatsoever.␈α∂Don't␈α∂dismiss␈α∂this␈α∂example␈α∂just␈α∂because␈α∂no-one
␈↓ ↓Hwould␈α∞write␈α∞such␈α
an␈α
obviously␈α
useless␈α
function␈α
definition.␈α
There␈α
is␈α
a␈α
sense␈α
in␈α
which␈α
it␈α
is␈α
the␈α
"zero"␈α
of␈α
a
␈↓ ↓Hlarge␈α⊃class␈α⊃of␈α⊃non¬terminating␈α⊃function␈α⊃definitions,␈α⊃and,␈α⊃as␈α⊃the␈α⊃Romans␈α⊂experienced␈α⊂but␈α⊂never␈α⊂learned,
␈↓ ↓Hleaving␈α
zero␈α
out␈α
of␈α
the␈α
number␈α
system␈α
is␈α
a␈α
mistake.

␈↓ α_Nevertheless,␈αin␈αmost␈αprogramming,␈αnon-terminating␈αcalculations␈αare␈αthe␈αresults␈αof␈α
errors␈α
in␈α
defining
␈↓ ↓Hfunctions.␈α
Therefore,␈α
it␈αwould␈αbe␈αuseful␈αto␈αbe␈αable␈αto␈αtell␈αwhether␈αa␈αfunction␈αdefinition␈αgives␈αa␈αresult␈αfor
␈↓ ↓Hall␈αarguments.␈αIn␈αfact,␈αit␈αwould␈αbe␈αuseful␈αto␈αbe␈αable␈αto␈αtell␈αwhether␈αa␈αfunction␈αwill␈αterminate␈αfor␈αa␈αsingle
␈↓ ↓Hargument.␈α
Let␈α
us␈α
make␈α
this␈α
goal␈α
more␈α
precise.

␈↓ α_Suppose␈αthat␈α␈↓↓f␈↓␈αis␈αa␈αLISP␈αfunction␈αand␈α␈↓↓a␈↓␈αis␈αan␈αS-expression,␈αand␈αwe␈αwould␈αlike␈αto␈αknow␈αwhether␈αthe
␈↓ ↓Hcomputation␈α
of␈α
␈↓↓f[a]␈↓␈αterminates.␈αSuppose␈α␈↓↓f␈↓␈αis␈αrepresented␈αby␈αthe␈αS-expression␈α␈↓↓f*␈↓␈αin␈αthe␈αusual␈αS-expression
␈↓ ↓Hnotation␈α∂for␈α∞LISP␈α∞functions.␈α∞Then␈α∞the␈α∞S-expression␈α∞␈↓↓(f*␈α∞(QUOTE␈α∞a))␈↓␈α∞represents␈α∞␈↓↓f[a]␈↓.␈α∞Define␈α∞the␈α∞function
␈↓ ↓H␈↓↓term␈↓␈αby␈αgiving␈α␈↓↓term[e]␈↓␈αthe␈αvalue␈α␈↓αtrue␈↓↓␈αif␈α␈↓↓e␈↓␈αis␈αan␈αS-expression␈αof␈αthe␈αform␈α␈↓↓(f*␈α(QUOTE␈αa))␈↓␈αfor␈αwhich␈α␈↓↓f[a]␈↓
␈↓ ↓Hterminates␈αand␈α␈↓αfalse␈↓␈αotherwise.␈αWe␈αnow␈αask␈α
whether␈α
␈↓↓term␈↓␈α
is␈α
a␈α
LISP␈α
function,␈α
i.e.␈α
can␈α
it␈α
be␈α
constructed␈α
from
␈↓ ↓H␈↓↓car,␈α
cdr,␈α
cons,␈α
atom,␈↓␈α
and␈α
␈↓↓eq␈↓␈α
using␈α
λ,␈α
␈↓αlabel␈↓,␈α
and␈α
conditional␈αexpressions?␈αWell,␈αit␈αcan't,␈αas␈αwe␈αshall␈αshortly
␈↓ ↓Hprove,␈αand␈αthis␈αmeans␈αthat␈αit␈αis␈αnot␈α␈↓↓computable␈↓␈αwhether␈αa␈αLISP␈αcalculation␈αterminates,␈αsince␈αif␈α␈↓↓term␈↓␈αwere
␈↓ ↓Hcomputable␈αby␈αany␈αcomputer␈αor␈αin␈αany␈αrecognized␈αsense,␈αit␈αcould␈αbe␈αrepresented␈αas␈αa␈αLISP␈αfunction.␈α
Here␈α
is
␈↓ ↓Hthe␈α
proof:

␈↓ ↓H
␈↓ α_Consider the function ␈↓↓terma␈↓ defined from ␈↓↓term␈↓ by
␈↓ ↓H

␈↓ ↓H
␈↓ α_␈↓↓terma u ← ␈↓αif␈↓↓ term list[u,list[␈↓QUOTE␈↓↓,u]] ␈↓αthen␈↓↓ loop u ␈↓αelse true␈↓,
␈↓ ↓H

␈↓ ↓H
␈↓ ↓Hand␈α∞suppose␈α∞that␈α
␈↓↓f␈↓␈α
is␈α
a␈α
LISP␈α
function␈α
and␈α
that␈α
␈↓↓f*␈↓␈α
is␈α
its␈α
S-expression␈α
representation.␈α
What␈α
is␈α
␈↓↓terma␈α
f*␈↓?
␈↓ ↓HWell␈α
␈↓↓terma␈α
f*␈↓␈α
tells␈α
us␈α
whether␈α
the␈α
computation␈α
of␈α
␈↓↓f[f*]␈↓␈α
terminates,␈α
and␈α
it␈α
tells␈α
us␈α
this␈α
by␈αgoing␈αinto␈αa
␈↓ ↓Hloop␈α
if␈α
␈↓↓f[f*]␈↓␈α
terminates␈α
and␈α
giving␈α
␈↓αtrue␈↓␈α
otherwise.␈α
Now␈α
if␈α
␈↓↓term␈↓␈αwere␈αa␈αLISP␈αfunction,␈αthen␈α␈↓↓terma␈↓␈αwould
␈↓ ↓Halso␈αbe␈αa␈αLISP␈αfunction.␈αIndeed␈αif␈α␈↓↓term␈↓␈αwere␈αrepresented␈αby␈αthe␈αS-expression␈α␈↓↓term*␈↓,␈αthen␈α␈↓↓terma␈↓␈αwould␈αbe
␈↓ ↓Hrepresented␈α
by␈α
the␈α
S-expression

␈↓ ↓H
␈↓ α_␈↓↓terma␈↓* = (LAMBDA (U) (COND ((␈↓↓term*␈↓ (LIST U (LIST (QUOTE QUOTE) U))) (LOOP U)) (T T))).
␈↓ ↓H

␈↓ ↓H
␈↓ ↓HNow␈αconsider␈α␈↓↓terma[terma*]␈↓.␈α
According␈α
to␈α
the␈α
definition␈α
of␈α
␈↓↓terma␈↓,␈α
this␈α
will␈α
tell␈α
us␈α
whether␈α
␈↓↓terma[terma*]␈↓
␈↓ ↓His␈α∃defined,␈α∃i.e.␈α∀it␈α∀tells␈α∀about␈α∀itself.␈α∀However,␈α∀it␈α∀gives␈α∀this␈α∀answer␈α∀in␈α∀a␈α∀contradictory␈α∀way;␈α∀namely
␈↓ ↓H␈↓↓terma[terma*]␈↓␈αlooping␈α
tells␈α
us␈α
that␈α
␈↓↓terma[terma*]␈↓␈α
terminates,␈α
and␈α
␈↓↓terma[terma*]␈↓␈α
being␈α
␈↓αtrue␈↓↓␈α
tells␈α
us␈α
that
␈↓ ↓H␈↓↓terma[terma*]␈↓␈αdoesn't␈αterminate.␈αThis␈αcontradiction␈αtells␈αus␈αthat␈α␈↓↓term␈↓␈αis␈αnot␈αa␈αLISP␈αfunction,␈αand␈αthere␈αis
␈↓ ↓Hno␈α
general␈α
procedure␈α
for␈α
telling␈α
whether␈α
a␈α
LISP␈α
calculation␈α
terminates.

␈↓ α_The␈α
above␈α
result␈α
does␈α
not␈α
exclude␈α
LISP␈α
functions␈α
that␈α
tell␈α
whether␈α
LISP␈αcalculations␈αterminate.␈αIt
␈↓ ↓Hjust␈α∩excludes␈α∩perfect␈α∩ones.␈α∩Suppose␈α∩we␈α∩have␈α∩a␈α∩function␈α⊃␈↓↓t␈↓␈α⊃that␈α⊃sometimes␈α⊃says␈α⊃calculations␈α⊃terminate,
␈↓ ↓Hsometimes␈αsays␈αthey␈αdon't␈αterminate,␈α
and␈α
sometimes␈α
runs␈α
on␈α
indefinitely.␈α
We␈α
shall␈α
further␈α
assume␈α
that␈α
when
␈↓ ↓H␈↓↓t␈↓␈α
gives␈α
an␈α
answer␈α
it␈α
is␈α
always␈α
right.␈α
Given␈αsuch␈αa␈αfunction␈αwe␈αcan␈αimprove␈αit␈αa␈αbit␈αso␈αthat␈αit␈αwill␈αalways
␈↓ ↓Hgive␈α⊃the␈α⊃right␈α⊃answer␈α⊃when␈α⊃the␈α⊃calculation␈α⊃it␈α⊃is␈α⊃asked␈α⊂about␈α⊂terminates.␈α⊂This␈α⊂is␈α⊂done␈α⊂by␈α⊂mixing␈α⊂the
␈↓ ↓Hcomputation␈α∃of␈α∃␈↓↓t[e]␈↓␈α∃with␈α∃a␈α∃computation␈α∃of␈α∃␈↓↓eval[e,␈↓NIL]␈α∃doing␈α∃the␈α∀computations␈α∀alternately.␈α∀If␈α∀the
␈↓ ↓H␈↓↓eval[e,␈↓NIL]␈α
computation␈α
ever␈α
terminates,␈α
then␈α
the␈α
new␈α
function␈α
asserts␈α
termination.

␈↓ α_Given␈α
such␈α
a␈α
␈↓↓t␈↓,␈α
we␈α
can␈α
always␈α
find␈α
a␈α
calculation␈α
that␈α
does␈α
not␈α
terminate␈α
but␈α
␈↓↓t␈↓␈α
doesn't␈αsay␈αso.␈αThe
␈↓ ↓Hconstruction␈α
is␈α
just␈α
like␈α
that␈α
used␈α
in␈α
the␈α
previous␈α
proof.␈α
Given␈α
␈↓↓t␈↓,␈α
we␈α
construct

␈↓ ↓H
␈↓ α_␈↓↓ta u ← ␈↓αif␈↓↓ t list[u,list[␈↓QUOTE␈↓↓,u]] ␈↓αthen␈↓↓ loop u ␈↓αelse true␈↓,
␈↓ ↓H

␈↓ ↓H
␈↓ ↓Hand␈αthen␈αwe␈αconsider␈α␈↓↓ta[ta*]␈↓.␈αIf␈αthis␈αhad␈αthe␈αvalue␈α␈↓αtrue␈↓,␈αthen␈αit␈αwouldn't␈αterminate␈αso␈αtherefore␈αit␈αdoesn't
␈↓ ↓Hterminate␈α
but␈α
is␈α
not␈α
one␈α
of␈α
those␈α
expressions␈α
which␈α
␈↓↓t␈↓␈α
decides.␈α
Thus␈α
for␈α
any␈αpartial␈αdecider␈αwe␈αcan␈αfind␈αa
␈↓ ↓HLISP␈α
calculation␈α
which␈α
doesn't␈α
terminate␈α
but␈α
which␈α
the␈α
decider␈α
doesn't␈α
decide.

␈↓ α_This␈α
can␈α
in␈α
turn␈α
be␈α
used␈α
to␈α
get␈α
a␈α
slightly␈α
better␈α
decider,␈α
namely

␈↓ ↓H
␈↓ α_␈↓↓t␈↓β1␈↓↓[e] ← ␈↓αif␈↓↓ e = ta* ␈↓αthen ␈↓DOESN'T-TERMINATE ␈↓αelse␈↓↓ t[e]␈↓.
␈↓ ↓H

␈↓ ↓H
␈↓ ↓HOf␈αcourse,␈α␈↓↓t␈↓β1␈↓␈αisn't␈α
much␈α
better␈α
than␈α
␈↓↓t␈↓,␈α
since␈α
it␈α
can␈α
decide␈α
only␈α
one␈α
more␈α
computation,␈α
but␈α
we␈α
can␈α
form␈α
␈↓↓t␈↓β2␈↓␈α
by
␈↓ ↓Happlying␈αthe␈αsame␈αprocess,␈αand␈αso␈αforth.␈αIn␈αfact,␈αwe␈αcan␈αeven␈αform␈α␈↓↓t␈↓β∞␈↓␈αwhich␈α
decides␈α
all␈α
the␈α
cases␈α
decided␈α
by
␈↓ ↓Hany␈α␈↓↓t␈↓βn␈↓.␈αThis␈αcan␈αbe␈αfurther␈αimproved␈αby␈αthe␈αsame␈αprocess,␈αetc.␈αHow␈αfar␈αcan␈αwe␈α
go?␈α
The␈α
answer␈α
is␈α
technical;
␈↓ ↓Hnamely,␈α
the␈α
improvement␈α
process␈α
can␈α
be␈α
carried␈α
out␈α
any␈α
recursive␈α
ordinal␈α
number␈α
of␈α
times.

␈↓ α_Unfortunately,␈αthis␈αkind␈αof␈αimprovement␈αseems␈αto␈αbe␈αsuperficial,␈αsince␈αnone␈αof␈αthe␈αnew␈αcomputations
␈↓ ↓Hproved␈α
not␈α
to␈α
terminate␈α
are␈α
likely␈α
to␈α
be␈α
of␈α
practical␈α
interest.

␈↓ ↓H
Exercises.
␈↓ ↓H

␈↓ ↓H
1. Write a function that gives ␈↓↓t␈↓βn+1␈↓ in terms of ␈↓↓t␈↓βn␈↓.
␈↓ ↓H

␈↓ ↓H
2. Write a function that gives ␈↓↓t␈↓β∞␈↓ in terms of ␈↓↓t␈↓.
␈↓ ↓H